The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))

Rewrite Strategy: FULL

(1) CpxTrsToCpxRelTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to relative TRS where S is empty.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))

S is empty.
Rewrite Strategy: FULL

(3) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
filterlow(n, cons(0, xs)) →⁺ filterlow(n, xs)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [xs / cons(0, xs)].
The result substitution is [ ].

(4) BOUNDS(n^1, INF)